Nuprl Lemma : fun-connected_antisymmetry
11,40
postcript
pdf
T
:Type,
f
:(
T
T
). retraction(
T
;
f
)
(
x
,
y
:
T
.
y
is
f
*(
x
)
x
is
f
*(
y
)
(
x
=
y
))
latex
Definitions
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
retraction(
T
;
f
)
,
Type
,
t
T
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
y
is
f
*(
x
)
,
P
Q
,
f
(
a
)
,
type
List
,
y
=
f
*(
x
) via
L
,
a
<
b
,
left
+
right
,
P
Q
,
Lemmas
retraction-fun-path
,
fun-connected
wf
,
retraction
wf
origin
T:Type, f:(T
T). retraction(T;f) 
(x, y:T. y is f*(x) x is f*(y) (x = y)) T:Type, f:(TT). retraction(T;f) (x, y:T. y is f*(x) x is f*(y) (x = y)) 
B(x)
x:A. B(x)
TB(x)x:A. B(x) Q
Q